Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
active(f(x)) |
→ mark(x) |
| 2: |
|
top(active(c)) |
→ top(mark(c)) |
| 3: |
|
top(mark(x)) |
→ top(check(x)) |
| 4: |
|
check(f(x)) |
→ f(check(x)) |
| 5: |
|
check(x) |
→ start(match(f(X),x)) |
| 6: |
|
match(f(x),f(y)) |
→ f(match(x,y)) |
| 7: |
|
match(X,x) |
→ proper(x) |
| 8: |
|
proper(c) |
→ ok(c) |
| 9: |
|
proper(f(x)) |
→ f(proper(x)) |
| 10: |
|
f(ok(x)) |
→ ok(f(x)) |
| 11: |
|
start(ok(x)) |
→ found(x) |
| 12: |
|
f(found(x)) |
→ found(f(x)) |
| 13: |
|
top(found(x)) |
→ top(active(x)) |
| 14: |
|
active(f(x)) |
→ f(active(x)) |
| 15: |
|
f(mark(x)) |
→ mark(f(x)) |
|
There are 20 dependency pairs:
|
| 16: |
|
TOP(active(c)) |
→ TOP(mark(c)) |
| 17: |
|
TOP(mark(x)) |
→ TOP(check(x)) |
| 18: |
|
TOP(mark(x)) |
→ CHECK(x) |
| 19: |
|
CHECK(f(x)) |
→ F(check(x)) |
| 20: |
|
CHECK(f(x)) |
→ CHECK(x) |
| 21: |
|
CHECK(x) |
→ START(match(f(X),x)) |
| 22: |
|
CHECK(x) |
→ MATCH(f(X),x) |
| 23: |
|
CHECK(x) |
→ F(X) |
| 24: |
|
MATCH(f(x),f(y)) |
→ F(match(x,y)) |
| 25: |
|
MATCH(f(x),f(y)) |
→ MATCH(x,y) |
| 26: |
|
MATCH(X,x) |
→ PROPER(x) |
| 27: |
|
PROPER(f(x)) |
→ F(proper(x)) |
| 28: |
|
PROPER(f(x)) |
→ PROPER(x) |
| 29: |
|
F(ok(x)) |
→ F(x) |
| 30: |
|
F(found(x)) |
→ F(x) |
| 31: |
|
TOP(found(x)) |
→ TOP(active(x)) |
| 32: |
|
TOP(found(x)) |
→ ACTIVE(x) |
| 33: |
|
ACTIVE(f(x)) |
→ F(active(x)) |
| 34: |
|
ACTIVE(f(x)) |
→ ACTIVE(x) |
| 35: |
|
F(mark(x)) |
→ F(x) |
|
The approximated dependency graph contains 6 SCCs:
{29,30,35},
{34},
{28},
{25},
{20}
and {16,17,31}.
-
Consider the SCC {29,30,35}.
There are no usable rules.
By taking the AF π with
π(F) = π(found) = π(mark) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {30,35}
are weakly decreasing and
rule 29
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {30,35}.
By taking the AF π with
π(F) = π(found) = 1 together with
the lexicographic path order with
empty precedence,
rule 30
is weakly decreasing and
rule 35
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {30}.
By taking the AF π with
π(F) = 1 together with
the lexicographic path order with
empty precedence,
rule 30
is strictly decreasing.
-
Consider the SCC {34}.
There are no usable rules.
By taking the AF π with
π(ACTIVE) = 1 together with
the lexicographic path order with
empty precedence,
rule 34
is strictly decreasing.
-
Consider the SCC {28}.
There are no usable rules.
By taking the AF π with
π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 28
is strictly decreasing.
-
Consider the SCC {25}.
There are no usable rules.
By taking the AF π with
π(MATCH) = 1 together with
the lexicographic path order with
empty precedence,
rule 25
is strictly decreasing.
-
Consider the SCC {20}.
There are no usable rules.
By taking the AF π with
π(CHECK) = 1 together with
the lexicographic path order with
empty precedence,
rule 20
is strictly decreasing.
-
Consider the SCC {16,17,31}.
The usable rules are {1,4-12,14,15}.
The constraints could not be solved.
Tyrolean Termination Tool (2.18 seconds)
--- May 3, 2006